0 CpxTRS
↳1 NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxTRS
↳3 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxWeightedTrs
↳5 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CpxTypedWeightedTrs
↳7 CompletionProof (UPPER BOUND(ID), 0 ms)
↳8 CpxTypedWeightedCompleteTrs
↳9 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳10 CpxRNTS
↳11 CompleteCoflocoProof (⇔, 1451 ms)
↳12 BOUNDS(1, n^2)
Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Concat(Id, s) → s
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s)) [1]
Concat(Id, s) → s [1]
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s) [1]
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t)) [1]
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s) [1]
Term_sub(Term_var(x), Id) → Term_var(x) [1]
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m [1]
Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s) [1]
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s)) [1]
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s)) [1]
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s) [1]
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s)) [1]
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t)) [1]
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s)) [1]
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s) [1]
Sum_sub(xi, Id) → Sum_term_var(xi) [1]
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k) [1]
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s) [1]
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s) [1]
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s)) [1]
Concat(Id, s) → s [1]
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s) [1]
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t)) [1]
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s) [1]
Term_sub(Term_var(x), Id) → Term_var(x) [1]
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m [1]
Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s) [1]
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s)) [1]
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s)) [1]
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s) [1]
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s)) [1]
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t)) [1]
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s)) [1]
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s) [1]
Sum_sub(xi, Id) → Sum_term_var(xi) [1]
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k) [1]
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s) [1]
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s) [1]
| Term_sub :: Term_pair:Term_var:Case:Term_app:Term_inl:Term_inr → Id:Cons_sum:Cons_usual → Term_pair:Term_var:Case:Term_app:Term_inl:Term_inr Term_pair :: Term_pair:Term_var:Case:Term_app:Term_inl:Term_inr → Term_pair:Term_var:Case:Term_app:Term_inl:Term_inr → Term_pair:Term_var:Case:Term_app:Term_inl:Term_inr Concat :: Id:Cons_sum:Cons_usual → Id:Cons_sum:Cons_usual → Id:Cons_sum:Cons_usual Id :: Id:Cons_sum:Cons_usual Sum_sub :: a → Id:Cons_sum:Cons_usual → Sum_term_var:Sum_constant Cons_sum :: b → Left:Right → Id:Cons_sum:Cons_usual → Id:Cons_sum:Cons_usual Cons_usual :: c → Term_pair:Term_var:Case:Term_app:Term_inl:Term_inr → Id:Cons_sum:Cons_usual → Id:Cons_sum:Cons_usual Term_var :: d → Term_pair:Term_var:Case:Term_app:Term_inl:Term_inr Case :: Term_pair:Term_var:Case:Term_app:Term_inl:Term_inr → a → Term_pair:Term_var:Case:Term_app:Term_inl:Term_inr → Term_pair:Term_var:Case:Term_app:Term_inl:Term_inr Frozen :: Term_pair:Term_var:Case:Term_app:Term_inl:Term_inr → Sum_term_var:Sum_constant → Term_pair:Term_var:Case:Term_app:Term_inl:Term_inr → Id:Cons_sum:Cons_usual → Term_pair:Term_var:Case:Term_app:Term_inl:Term_inr Term_app :: Term_pair:Term_var:Case:Term_app:Term_inl:Term_inr → Term_pair:Term_var:Case:Term_app:Term_inl:Term_inr → Term_pair:Term_var:Case:Term_app:Term_inl:Term_inr Sum_term_var :: a → Sum_term_var:Sum_constant Term_inl :: Term_pair:Term_var:Case:Term_app:Term_inl:Term_inr → Term_pair:Term_var:Case:Term_app:Term_inl:Term_inr Term_inr :: Term_pair:Term_var:Case:Term_app:Term_inl:Term_inr → Term_pair:Term_var:Case:Term_app:Term_inl:Term_inr Sum_constant :: Left:Right → Sum_term_var:Sum_constant Left :: Left:Right Right :: Left:Right |
Term_sub(v0, v1) → null_Term_sub [0]
Frozen(v0, v1, v2, v3) → null_Frozen [0]
null_Term_sub, null_Frozen, const, const1, const2, const3, const4
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
Id => 0
Left => 0
Right => 1
null_Term_sub => 0
null_Frozen => 0
const => 0
const1 => 0
const2 => 0
const3 => 0
const4 => 0
Concat(z, z') -{ 1 }→ s :|: s >= 0, z = 0, z' = s
Concat(z, z') -{ 1 }→ 1 + x + Term_sub(m, t) + Concat(s, t) :|: z' = t, x >= 0, t >= 0, s >= 0, z = 1 + x + m + s, m >= 0
Concat(z, z') -{ 1 }→ 1 + xi + k + Concat(s, t) :|: z' = t, t >= 0, k >= 0, s >= 0, z = 1 + xi + k + s, xi >= 0
Frozen(z, z', z'', z1) -{ 1 }→ Term_sub(m, s) :|: z = m, n >= 0, z'' = n, z1 = s, z' = 1 + 0, s >= 0, m >= 0
Frozen(z, z', z'', z1) -{ 1 }→ Term_sub(n, s) :|: z = m, z' = 1 + 1, n >= 0, z'' = n, z1 = s, s >= 0, m >= 0
Frozen(z, z', z'', z1) -{ 0 }→ 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
Frozen(z, z', z'', z1) -{ 1 }→ 1 + Term_sub(m, s) + xi + Term_sub(n, s) :|: z = m, n >= 0, z'' = n, z1 = s, z' = 1 + xi, s >= 0, xi >= 0, m >= 0
Sum_sub(z, z') -{ 1 }→ Sum_sub(xi, s) :|: z' = 1 + psi + k + s, z = xi, psi >= 0, k >= 0, s >= 0, xi >= 0
Sum_sub(z, z') -{ 1 }→ Sum_sub(xi, s) :|: y >= 0, z = xi, z' = 1 + y + m + s, s >= 0, xi >= 0, m >= 0
Sum_sub(z, z') -{ 1 }→ 1 + k :|: z' = 1 + psi + k + s, z = xi, psi >= 0, k >= 0, s >= 0, xi >= 0
Sum_sub(z, z') -{ 1 }→ 1 + xi :|: z = xi, xi >= 0, z' = 0
Term_sub(z, z') -{ 1 }→ m :|: x >= 0, y >= 0, z = 1 + x, z' = 1 + y + m + s, s >= 0, m >= 0
Term_sub(z, z') -{ 1 }→ Term_sub(1 + x, s) :|: z' = 1 + xi + k + s, x >= 0, z = 1 + x, k >= 0, s >= 0, xi >= 0
Term_sub(z, z') -{ 1 }→ Term_sub(1 + x, s) :|: x >= 0, y >= 0, z = 1 + x, z' = 1 + y + m + s, s >= 0, m >= 0
Term_sub(z, z') -{ 1 }→ Frozen(m, Sum_sub(xi, s), n, s) :|: z = 1 + m + xi + n, n >= 0, s >= 0, z' = s, xi >= 0, m >= 0
Term_sub(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
Term_sub(z, z') -{ 1 }→ 1 + x :|: x >= 0, z = 1 + x, z' = 0
Term_sub(z, z') -{ 1 }→ 1 + Term_sub(m, s) :|: s >= 0, z' = s, z = 1 + m, m >= 0
Term_sub(z, z') -{ 1 }→ 1 + Term_sub(m, s) + Term_sub(n, s) :|: n >= 0, z = 1 + m + n, s >= 0, z' = s, m >= 0
| eq(start(V, V1, V27, V28),0,[fun(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V27, V28),0,[fun1(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V27, V28),0,[fun2(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V27, V28),0,[fun3(V, V1, V27, V28, Out)],[V >= 0,V1 >= 0,V27 >= 0,V28 >= 0]). eq(fun(V, V1, Out),1,[fun(V2, V3, Ret01),fun(V4, V3, Ret1)],[Out = 1 + Ret01 + Ret1,V4 >= 0,V = 1 + V2 + V4,V3 >= 0,V1 = V3,V2 >= 0]). eq(fun1(V, V1, Out),1,[],[Out = V5,V5 >= 0,V = 0,V1 = V5]). eq(fun2(V, V1, Out),1,[fun2(V6, V7, Ret)],[Out = Ret,V1 = 1 + V7 + V8 + V9,V = V6,V8 >= 0,V9 >= 0,V7 >= 0,V6 >= 0]). eq(fun1(V, V1, Out),1,[fun(V11, V12, Ret011),fun1(V13, V12, Ret11)],[Out = 1 + Ret011 + Ret11 + V10,V1 = V12,V10 >= 0,V12 >= 0,V13 >= 0,V = 1 + V10 + V11 + V13,V11 >= 0]). eq(fun(V, V1, Out),1,[fun(1 + V14, V15, Ret2)],[Out = Ret2,V1 = 1 + V15 + V16 + V17,V14 >= 0,V = 1 + V14,V17 >= 0,V15 >= 0,V16 >= 0]). eq(fun(V, V1, Out),1,[],[Out = 1 + V18,V18 >= 0,V = 1 + V18,V1 = 0]). eq(fun(V, V1, Out),1,[],[Out = V19,V20 >= 0,V21 >= 0,V = 1 + V20,V1 = 1 + V19 + V21 + V22,V22 >= 0,V19 >= 0]). eq(fun(V, V1, Out),1,[fun2(V24, V25, Ret12),fun3(V23, Ret12, V26, V25, Ret3)],[Out = Ret3,V = 1 + V23 + V24 + V26,V26 >= 0,V25 >= 0,V1 = V25,V24 >= 0,V23 >= 0]). eq(fun3(V, V1, V27, V28, Out),1,[fun(V29, V30, Ret001),fun(V32, V30, Ret13)],[Out = 1 + Ret001 + Ret13 + V31,V = V29,V32 >= 0,V27 = V32,V28 = V30,V1 = 1 + V31,V30 >= 0,V31 >= 0,V29 >= 0]). eq(fun2(V, V1, Out),1,[fun2(V33, V34, Ret4)],[Out = Ret4,V35 >= 0,V = V33,V1 = 1 + V34 + V35 + V36,V34 >= 0,V33 >= 0,V36 >= 0]). eq(fun(V, V1, Out),1,[fun(V37, V38, Ret14)],[Out = 1 + Ret14,V38 >= 0,V1 = V38,V = 1 + V37,V37 >= 0]). eq(fun1(V, V1, Out),1,[fun1(V41, V42, Ret15)],[Out = 1 + Ret15 + V39 + V40,V1 = V42,V42 >= 0,V40 >= 0,V41 >= 0,V = 1 + V39 + V40 + V41,V39 >= 0]). eq(fun3(V, V1, V27, V28, Out),1,[fun(V43, V44, Ret5)],[Out = Ret5,V = V43,V45 >= 0,V27 = V45,V28 = V44,V1 = 1,V44 >= 0,V43 >= 0]). eq(fun2(V, V1, Out),1,[],[Out = 1 + V46,V = V46,V46 >= 0,V1 = 0]). eq(fun2(V, V1, Out),1,[],[Out = 1 + V47,V1 = 1 + V47 + V48 + V49,V = V50,V48 >= 0,V47 >= 0,V49 >= 0,V50 >= 0]). eq(fun(V, V1, Out),1,[fun(1 + V51, V52, Ret6)],[Out = Ret6,V51 >= 0,V53 >= 0,V = 1 + V51,V1 = 1 + V52 + V53 + V54,V52 >= 0,V54 >= 0]). eq(fun3(V, V1, V27, V28, Out),1,[fun(V55, V56, Ret7)],[Out = Ret7,V = V57,V1 = 2,V55 >= 0,V27 = V55,V28 = V56,V56 >= 0,V57 >= 0]). eq(fun(V, V1, Out),0,[],[Out = 0,V58 >= 0,V59 >= 0,V = V58,V1 = V59]). eq(fun3(V, V1, V27, V28, Out),0,[],[Out = 0,V28 = V60,V61 >= 0,V27 = V62,V63 >= 0,V = V61,V1 = V63,V62 >= 0,V60 >= 0]). input_output_vars(fun(V,V1,Out),[V,V1],[Out]). input_output_vars(fun1(V,V1,Out),[V,V1],[Out]). input_output_vars(fun2(V,V1,Out),[V,V1],[Out]). input_output_vars(fun3(V,V1,V27,V28,Out),[V,V1,V27,V28],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. recursive : [fun2/3]
1. recursive [multiple] : [fun/3,fun3/5]
2. recursive : [fun1/3]
3. non_recursive : [start/4]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into fun2/3
1. SCC is partially evaluated into fun/3
2. SCC is partially evaluated into fun1/3
3. SCC is partially evaluated into start/4
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations fun2/3
* CE 24 is refined into CE [25]
* CE 23 is refined into CE [26]
* CE 22 is refined into CE [27]
### Cost equations --> "Loop" of fun2/3
* CEs [27] --> Loop 15
* CEs [25] --> Loop 16
* CEs [26] --> Loop 17
### Ranking functions of CR fun2(V,V1,Out)
* RF of phase [15]: [V1]
#### Partial ranking functions of CR fun2(V,V1,Out)
* Partial RF of phase [15]:
- RF of loop [15:1]:
V1
### Specialization of cost equations fun/3
* CE 16 is refined into CE [28]
* CE 9 is refined into CE [29,30,31]
* CE 18 is refined into CE [32]
* CE 15 is refined into CE [33]
* CE 10 is refined into CE [34,35,36]
* CE 11 is refined into CE [37,38,39]
* CE 14 is refined into CE [40]
* CE 17 is refined into CE [41]
* CE 12 is refined into CE [42,43,44]
* CE 13 is refined into CE [45]
### Cost equations --> "Loop" of fun/3
* CEs [44] --> Loop 18
* CEs [43] --> Loop 19
* CEs [45] --> Loop 20
* CEs [42] --> Loop 21
* CEs [35,36,38,39] --> Loop 22
* CEs [40] --> Loop 23
* CEs [41] --> Loop 24
* CEs [34,37] --> Loop 25
* CEs [28] --> Loop 26
* CEs [33] --> Loop 27
* CEs [29,30,31,32] --> Loop 28
### Ranking functions of CR fun(V,V1,Out)
* RF of phase [18,19,20,21,22,23,24,25]: [V+V1]
#### Partial ranking functions of CR fun(V,V1,Out)
* Partial RF of phase [18,19,20,21,22,23,24,25]:
- RF of loop [18:1,18:2,19:1,19:2,20:1,20:2,21:1,21:2,22:1,24:1,25:1]:
V
- RF of loop [23:1]:
V1
### Specialization of cost equations fun1/3
* CE 20 is refined into CE [46,47]
* CE 21 is refined into CE [48]
* CE 19 is refined into CE [49]
### Cost equations --> "Loop" of fun1/3
* CEs [49] --> Loop 29
* CEs [46] --> Loop 30
* CEs [47,48] --> Loop 31
### Ranking functions of CR fun1(V,V1,Out)
* RF of phase [30,31]: [V]
#### Partial ranking functions of CR fun1(V,V1,Out)
* Partial RF of phase [30,31]:
- RF of loop [30:1]:
V-1
- RF of loop [31:1]:
V
### Specialization of cost equations start/4
* CE 3 is refined into CE [50,51]
* CE 2 is refined into CE [52]
* CE 4 is refined into CE [53,54]
* CE 5 is refined into CE [55,56,57,58]
* CE 6 is refined into CE [59,60]
* CE 7 is refined into CE [61,62]
* CE 8 is refined into CE [63,64,65]
### Cost equations --> "Loop" of start/4
* CEs [50,51] --> Loop 32
* CEs [53,54] --> Loop 33
* CEs [63] --> Loop 34
* CEs [52,55,56,57,58,59,60,61,62,64,65] --> Loop 35
### Ranking functions of CR start(V,V1,V27,V28)
#### Partial ranking functions of CR start(V,V1,V27,V28)
Computing Bounds
=====================================
#### Cost of chains of fun2(V,V1,Out):
* Chain [[15],17]: 1*it(15)+1
Such that:it(15) =< V1
with precondition: [V+1=Out,V>=0,V1>=1]
* Chain [[15],16]: 1*it(15)+1
Such that:it(15) =< V1-Out
with precondition: [V>=0,Out>=1,V1>=Out+1]
* Chain [17]: 1
with precondition: [V1=0,V+1=Out,V>=0]
* Chain [16]: 1
with precondition: [V>=0,Out>=1,V1>=Out]
#### Cost of chains of fun(V,V1,Out):
* Chain [28]: 2*s(2)+2
Such that:aux(1) =< V1
s(2) =< aux(1)
with precondition: [Out=0,V>=0,V1>=0]
* Chain [27]: 1
with precondition: [V1=0,V=Out,V>=1]
* Chain [26]: 1
with precondition: [V>=1,Out>=0,V1>=Out+1]
* Chain [multiple([18,19,20,21,22,23,24,25],[[28],[27],[26]])]: 10*it(18)+7*it(22)+1*it(23)+1*it([26])+1*it([27])+2*it([28])+1*s(16)+1*s(17)+4*s(18)+2*s(22)+0
Such that:it([28]) =< V+1
aux(10) =< V+2*V1
aux(33) =< V
aux(34) =< V+V1
aux(35) =< V/2+1/2
aux(36) =< V1
it(18) =< aux(33)
it(22) =< aux(33)
it([26]) =< aux(33)
it([27]) =< aux(33)
it([26]) =< aux(35)
it([27]) =< aux(35)
aux(5) =< aux(36)
aux(20) =< aux(36)*2
aux(11) =< aux(10)
aux(6) =< it(18)*aux(10)
s(16) =< it(18)*aux(36)
aux(16) =< it(18)*aux(20)
s(23) =< it([28])*aux(5)
aux(7) =< it(18)*aux(11)
s(17) =< it(18)*aux(5)
it(22) =< aux(7)+aux(7)+aux(6)+aux(34)
it(23) =< aux(7)+aux(7)+aux(6)+aux(34)
it([26]) =< aux(7)+aux(7)+aux(6)+aux(34)
it([27]) =< aux(7)+aux(7)+aux(6)+aux(34)
s(23) =< aux(7)+aux(7)+aux(6)+aux(34)
it(23) =< aux(16)+aux(16)+aux(16)+aux(36)
it([26]) =< aux(16)+aux(16)+aux(16)+aux(36)
s(23) =< aux(16)+aux(16)+aux(16)+aux(36)
s(20) =< it(22)*aux(5)
s(22) =< s(23)
s(18) =< s(20)
with precondition: [V>=1,V1>=0,Out>=0]
#### Cost of chains of fun1(V,V1,Out):
* Chain [[30,31],29]: 17*it(30)+7*s(97)+1*s(98)+1*s(99)+1*s(100)+1*s(101)+1*s(102)+2*s(103)+4*s(104)+2*s(114)+1
Such that:aux(38) =< V+V1
s(71) =< V+2*V1
s(73) =< V1
aux(44) =< V
it(30) =< aux(44)
aux(40) =< s(73)
s(112) =< aux(44)* (1/2)
s(109) =< it(30)*aux(38)
s(107) =< it(30)*aux(40)
s(114) =< s(107)
s(97) =< aux(44)
s(98) =< aux(44)
s(99) =< aux(44)
s(98) =< s(112)
s(99) =< s(112)
s(80) =< s(73)*2
s(81) =< s(71)
s(110) =< it(30)*s(71)
s(100) =< it(30)*s(73)
s(108) =< it(30)*s(80)
s(106) =< it(30)*aux(40)
s(111) =< it(30)*s(81)
s(101) =< it(30)*aux(40)
s(97) =< s(111)+s(111)+s(110)+s(109)
s(102) =< s(111)+s(111)+s(110)+s(109)
s(98) =< s(111)+s(111)+s(110)+s(109)
s(99) =< s(111)+s(111)+s(110)+s(109)
s(106) =< s(111)+s(111)+s(110)+s(109)
s(102) =< s(108)+s(108)+s(108)+s(107)
s(98) =< s(108)+s(108)+s(108)+s(107)
s(106) =< s(108)+s(108)+s(108)+s(107)
s(105) =< s(97)*aux(40)
s(103) =< s(106)
s(104) =< s(105)
with precondition: [V>=1,V1>=0,Out>=V1+1]
* Chain [29]: 1
with precondition: [V=0,V1=Out,V1>=0]
#### Cost of chains of start(V,V1,V27,V28):
* Chain [35]: 6*s(117)+47*s(122)+14*s(123)+2*s(124)+2*s(125)+2*s(130)+2*s(134)+2*s(135)+4*s(137)+8*s(138)+4*s(140)+20*s(145)+14*s(146)+2*s(147)+2*s(148)+2*s(153)+2*s(157)+2*s(158)+4*s(160)+8*s(161)+8*s(186)+7*s(223)+1*s(224)+1*s(225)+2*s(230)+2*s(234)+1*s(235)+2*s(237)+4*s(238)+4*s(240)+2*s(250)+7*s(251)+1*s(252)+1*s(253)+1*s(262)+2*s(264)+4*s(265)+5
Such that:aux(49) =< V
aux(50) =< V+1
aux(51) =< V+V1
aux(52) =< V+2*V1
aux(53) =< V+V28
aux(54) =< V+2*V28
aux(55) =< V/2+1/2
aux(56) =< V1
aux(57) =< V27
aux(58) =< V27+1
aux(59) =< V27+V28
aux(60) =< V27+2*V28
aux(61) =< V27/2+1/2
aux(62) =< V28
s(117) =< aux(50)
s(240) =< aux(56)
s(140) =< aux(58)
s(145) =< aux(57)
s(146) =< aux(57)
s(147) =< aux(57)
s(148) =< aux(57)
s(147) =< aux(61)
s(148) =< aux(61)
s(126) =< aux(62)
s(127) =< aux(62)*2
s(151) =< aux(60)
s(152) =< s(145)*aux(60)
s(153) =< s(145)*aux(62)
s(154) =< s(145)*s(127)
s(155) =< s(140)*s(126)
s(156) =< s(145)*s(151)
s(157) =< s(145)*s(126)
s(146) =< s(156)+s(156)+s(152)+aux(59)
s(158) =< s(156)+s(156)+s(152)+aux(59)
s(147) =< s(156)+s(156)+s(152)+aux(59)
s(148) =< s(156)+s(156)+s(152)+aux(59)
s(155) =< s(156)+s(156)+s(152)+aux(59)
s(158) =< s(154)+s(154)+s(154)+aux(62)
s(147) =< s(154)+s(154)+s(154)+aux(62)
s(155) =< s(154)+s(154)+s(154)+aux(62)
s(159) =< s(146)*s(126)
s(160) =< s(155)
s(161) =< s(159)
s(122) =< aux(49)
s(123) =< aux(49)
s(124) =< aux(49)
s(125) =< aux(49)
s(124) =< aux(55)
s(125) =< aux(55)
s(128) =< aux(54)
s(129) =< s(122)*aux(54)
s(130) =< s(122)*aux(62)
s(131) =< s(122)*s(127)
s(132) =< s(117)*s(126)
s(133) =< s(122)*s(128)
s(134) =< s(122)*s(126)
s(123) =< s(133)+s(133)+s(129)+aux(53)
s(135) =< s(133)+s(133)+s(129)+aux(53)
s(124) =< s(133)+s(133)+s(129)+aux(53)
s(125) =< s(133)+s(133)+s(129)+aux(53)
s(132) =< s(133)+s(133)+s(129)+aux(53)
s(135) =< s(131)+s(131)+s(131)+aux(62)
s(124) =< s(131)+s(131)+s(131)+aux(62)
s(132) =< s(131)+s(131)+s(131)+aux(62)
s(136) =< s(123)*s(126)
s(137) =< s(132)
s(138) =< s(136)
s(186) =< aux(62)
s(223) =< aux(49)
s(224) =< aux(49)
s(225) =< aux(49)
s(224) =< aux(55)
s(225) =< aux(55)
s(226) =< aux(56)
s(227) =< aux(56)*2
s(228) =< aux(52)
s(229) =< s(122)*aux(52)
s(230) =< s(122)*aux(56)
s(231) =< s(122)*s(227)
s(232) =< s(117)*s(226)
s(233) =< s(122)*s(228)
s(234) =< s(122)*s(226)
s(223) =< s(233)+s(233)+s(229)+aux(51)
s(235) =< s(233)+s(233)+s(229)+aux(51)
s(224) =< s(233)+s(233)+s(229)+aux(51)
s(225) =< s(233)+s(233)+s(229)+aux(51)
s(232) =< s(233)+s(233)+s(229)+aux(51)
s(235) =< s(231)+s(231)+s(231)+aux(56)
s(224) =< s(231)+s(231)+s(231)+aux(56)
s(232) =< s(231)+s(231)+s(231)+aux(56)
s(236) =< s(223)*s(226)
s(237) =< s(232)
s(238) =< s(236)
s(247) =< aux(49)* (1/2)
s(248) =< s(122)*aux(51)
s(249) =< s(122)*s(226)
s(250) =< s(249)
s(251) =< aux(49)
s(252) =< aux(49)
s(253) =< aux(49)
s(252) =< s(247)
s(253) =< s(247)
s(259) =< s(122)*s(226)
s(251) =< s(233)+s(233)+s(229)+s(248)
s(262) =< s(233)+s(233)+s(229)+s(248)
s(252) =< s(233)+s(233)+s(229)+s(248)
s(253) =< s(233)+s(233)+s(229)+s(248)
s(259) =< s(233)+s(233)+s(229)+s(248)
s(262) =< s(231)+s(231)+s(231)+s(249)
s(252) =< s(231)+s(231)+s(231)+s(249)
s(259) =< s(231)+s(231)+s(231)+s(249)
s(263) =< s(251)*s(226)
s(264) =< s(259)
s(265) =< s(263)
with precondition: [V>=0,V1>=0]
* Chain [34]: 1
with precondition: [V1=0,V>=0]
* Chain [33]: 2*s(269)+10*s(274)+7*s(275)+1*s(276)+1*s(277)+1*s(282)+1*s(286)+1*s(287)+2*s(289)+4*s(290)+2*s(292)+3
Such that:s(268) =< V
s(269) =< V+1
s(270) =< V+V28
s(271) =< V+2*V28
s(272) =< V/2+1/2
aux(63) =< V28
s(274) =< s(268)
s(275) =< s(268)
s(276) =< s(268)
s(277) =< s(268)
s(276) =< s(272)
s(277) =< s(272)
s(278) =< aux(63)
s(279) =< aux(63)*2
s(280) =< s(271)
s(281) =< s(274)*s(271)
s(282) =< s(274)*aux(63)
s(283) =< s(274)*s(279)
s(284) =< s(269)*s(278)
s(285) =< s(274)*s(280)
s(286) =< s(274)*s(278)
s(275) =< s(285)+s(285)+s(281)+s(270)
s(287) =< s(285)+s(285)+s(281)+s(270)
s(276) =< s(285)+s(285)+s(281)+s(270)
s(277) =< s(285)+s(285)+s(281)+s(270)
s(284) =< s(285)+s(285)+s(281)+s(270)
s(287) =< s(283)+s(283)+s(283)+aux(63)
s(276) =< s(283)+s(283)+s(283)+aux(63)
s(284) =< s(283)+s(283)+s(283)+aux(63)
s(288) =< s(275)*s(278)
s(289) =< s(284)
s(290) =< s(288)
s(292) =< aux(63)
with precondition: [V1=1,V>=0,V27>=0,V28>=0]
* Chain [32]: 2*s(294)+10*s(299)+7*s(300)+1*s(301)+1*s(302)+1*s(307)+1*s(311)+1*s(312)+2*s(314)+4*s(315)+2*s(317)+3
Such that:s(293) =< V27
s(294) =< V27+1
s(295) =< V27+V28
s(296) =< V27+2*V28
s(297) =< V27/2+1/2
aux(64) =< V28
s(299) =< s(293)
s(300) =< s(293)
s(301) =< s(293)
s(302) =< s(293)
s(301) =< s(297)
s(302) =< s(297)
s(303) =< aux(64)
s(304) =< aux(64)*2
s(305) =< s(296)
s(306) =< s(299)*s(296)
s(307) =< s(299)*aux(64)
s(308) =< s(299)*s(304)
s(309) =< s(294)*s(303)
s(310) =< s(299)*s(305)
s(311) =< s(299)*s(303)
s(300) =< s(310)+s(310)+s(306)+s(295)
s(312) =< s(310)+s(310)+s(306)+s(295)
s(301) =< s(310)+s(310)+s(306)+s(295)
s(302) =< s(310)+s(310)+s(306)+s(295)
s(309) =< s(310)+s(310)+s(306)+s(295)
s(312) =< s(308)+s(308)+s(308)+aux(64)
s(301) =< s(308)+s(308)+s(308)+aux(64)
s(309) =< s(308)+s(308)+s(308)+aux(64)
s(313) =< s(300)*s(303)
s(314) =< s(309)
s(315) =< s(313)
s(317) =< aux(64)
with precondition: [V1=2,V>=0,V27>=0,V28>=0]
Closed-form bounds of start(V,V1,V27,V28):
-------------------------------------
* Chain [35] with precondition: [V>=0,V1>=0]
- Upper bound: 83*V+4*V1+5+16*V1*V+ (V+1)* (2*V1)+nat(V27)*38+nat(V28)*8+nat(V28)*12*V+nat(V28)*12*nat(V27)+ (V+1)* (nat(V28)*4)+nat(V28)*4*nat(V27+1)+ (V+V1)+ (V+V1)*V+nat(V+V28)*2+ (6*V+6)+ (6*V+12*V1)*V+nat(V+2*V28)*6*V+nat(V27+V28)*2+nat(V27+1)*4+nat(V27+2*V28)*6*nat(V27)
- Complexity: n^2
* Chain [34] with precondition: [V1=0,V>=0]
- Upper bound: 1
- Complexity: constant
* Chain [33] with precondition: [V1=1,V>=0,V27>=0,V28>=0]
- Upper bound: 19*V+2*V28+3+6*V28*V+ (V+V28)+ (2*V+2)+ (2*V+2)*V28+ (3*V+6*V28)*V
- Complexity: n^2
* Chain [32] with precondition: [V1=2,V>=0,V27>=0,V28>=0]
- Upper bound: 19*V27+2*V28+3+6*V28*V27+ (V27+V28)+ (2*V27+2)+ (2*V27+2)*V28+ (3*V27+6*V28)*V27
- Complexity: n^2
### Maximum cost of start(V,V1,V27,V28): nat(V28)*2+2+max([nat(V28)*6*V+19*V+nat(V+V28)+ (2*V+2)+nat(V+2*V28)*3*V+max([ (2*V+2)*nat(V28),64*V+4*V1+2+16*V1*V+ (V+1)* (2*V1)+nat(V27)*38+nat(V28)*6+nat(V28)*6*V+nat(V28)*12*nat(V27)+ (V+1)* (nat(V28)*4)+nat(V28)*4*nat(V27+1)+ (V+V1)+ (V+V1)*V+nat(V+V28)+ (4*V+4)+ (6*V+12*V1)*V+nat(V+2*V28)*3*V+nat(V27+V28)*2+nat(V27+1)*4+nat(V27+2*V28)*6*nat(V27)]),nat(V28)*6*nat(V27)+nat(V27)*19+nat(V27+V28)+nat(V27+1)*2+nat(V27+1)*2*nat(V28)+nat(V27+2*V28)*3*nat(V27)])+1
Asymptotic class: n^2
* Total analysis performed in 1096 ms.